CI: use bash instead of python for proof checking #192
Conversation
Signed-off-by: Andrew Helwer <[email protected]>
| -and -not -wholename "*/LeastCircularSubstring/*" \ | ||
| -and -not -wholename "*/diskpaxos/*" \ | ||
| -and -not -wholename "*/ewd998/*" \ | ||
| -and -not -wholename "*/ewd840/*" \ |
There was a problem hiding this comment.
If I understand correctly, you pass all TLA+ modules to tlapm, except those mentioned here. Up to now, the logic was "positive" in the sense that only specifications that declared containing a proof were checked. For ewd840, the incriminated "ToString" operator is used only in EWD840_anim.tla, whereas as far as I can tell the exception list also contains EWD840_proof.tla, which it would be great to check. Similarly, ewd998/EWD998_proof.tla should pass the check but is excluded here?
There was a problem hiding this comment.
Yeah I think I am leaning against this approach after seeing how large the list will grow (probably at least double this size). There are a lot of examples that use the RECURSIVE keyword. All those EWD directories also have lots of files, most of which fail parsing since they use nonstandard TLC modules.
|
Closing this because the approach isn't quite there yet. I think I will need to implement a python script called something like is_proof.py that filters a pipeline of all .tla files found by |
2 participants
macOS runners also seem to be getting slower, so skip checking one of the CoffeeCan models.